00100	
00200	
00300	(DEFPROP ATTEMPT 
00400	 (LAMBDA(Z S C)
00500	  (PROG (NEWNAME SUPPORT
00600	 		 EDITSTRAT
00700	 		 LCL
00800	 		 LVL
00900	 		 CNT
01000	 		 XYZ2
01100	 		 LSTCLS
01200	 		 LLST
01300	 		 Z1
01400	 		 MERGE
01500	 		 ORDER
01600	 		 DEBUG
01700	 		 DEPTH
01800	 		 LENGTH
01900	 		 ANCESTRY
02000	 		 STRATEGY
02100	 		 STRAT
02200	 		 PMODEL
02300	 		 NMODEL
02400	 		 PFLG
02500	 		 PDEPTH
02600	 		 DLIST
02700	 		 XYZ
02800	 		 XYZ1
02900	 		 COND
03000	 		 UNAXP
03100	 		 UNAXN
03200	 		 SAT
03300	 		 EE
03400	 		 EE1
03500	 		 XX
03600	 		 CLAUSES
03700	 		 SUBCLAUSES
03800	 		 COUNT)
03900		(SETQ TBL (SET1 (APPEND PREFN INFN)))
04000		(SET3 Z)
04100		(SETQ Z (MINIMIZE Z))
04200		(SETQ NEWNAME (INITIAL Z))
04300		(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
04400		(SETQ COND C)
04500		(SETQ XYZ2 Z)
04600		(SETQ LVL 1)
04700		(SETQ COUNT 0)
04800		(SETQ Z (UNITPN XYZ2))
04900		(SETQ UNAXP (CAR Z))
05000		(SETQ UNAXN (CDR Z))
05100		(SETQ CLAUSES XYZ2)
05200		(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
05300				  (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
05400		      (T (SETQ SUBCLAUSES CLAUSES)))
05500		(SETQ LCL (LAST CLAUSES))
05600		(SETQ LSTCLS LCL)
05700		(COND (ANCESTRY (GO AA)))
05800		(SETQ XX (CONS CLAUSES CLAUSES))
05900		(SETQ EE CLAUSES)
06000		(SETQ EE1 (LAST EE))
06100		(SETQ CNT (LENGTH XYZ2))
06200	   BB   (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
06300		(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
06400		      ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
06500						       (EVAL
06600							(LIST (QUOTE OUTC)
06700							      (LIST (QUOTE OUTPUT)
06800								    (QUOTE PRF)
06900								    (QUOTE DSK:)
07000								    (CONS (READLIST
07100									   (CONS (QUOTE N)
07200										 (CONS (SETQ PRNO (ADD1 PRNO))
07300	 									       FILENAM)))
07400									  (QUOTE PRF)))
07500	 						      NIL)))
07600						 (QUERY)
07700						 (PROOF LHP RHP)
07800						 (OUTC Z T)
07900						 (RETURN Z1))
08000		      (T (RETURN Z1)))
08100	   AA   (SETQ XYZ XYZ2)
08200		(SETQ EE CLAUSES)
08300		(SETQ EE1 (LAST CLAUSES))
08400	   CC   (SETQ LLST (CONS (CAR XYZ) LLST))
08500		(SETQ XYZ (CDR XYZ))
08600		(COND (XYZ (GO CC)) (T (GO BB))))) 
08700	EXPR)
     

00100	
00200	
00300	(DEFPROP <INPUT> 
00400	 (LAMBDA NIL
00500	  (NLRR (QUOTE INPUT)
00600		(FUNCTION
00700		 (LAMBDA NIL
00800		  (COND ((AND (<DECOP>) (CH :) (<OPLIST>)) (CONS (STK 2) (STK 0)))
00900			((AND (<ID>) (CH :)) (STK 1))
01000			((AND (<S>)) (STK 0))
01100			(*NIL*)))))) 
01200	EXPR)
01300	
01400	(DEFPROP >INPUT< 
01500	 (LAMBDA(%N)
01600	  (OUTRUL %N
01700		  (FUNCTION
01800		   (LAMBDA NIL
01900		    (COND ((AND (MATCH (QUOTE (* . *))) (>DECOP< 1) (>OPLIST< 0)) (LIST (STK1) (QUOTE (:CH :)) (STK0)))
02000			  ((>S< 1) (STK1))
02100			  ((>ID< 1) (LIST (STK1) (QUOTE (:CH :))))))))) 
02200	EXPR)
02300	
02400	(DEFPROP <OPLIST> 
02500	 (LAMBDA NIL (NLRR (QUOTE OPLIST) (FUNCTION (LAMBDA NIL (COND ((AND (<OPL>) (CH ;)) (STK 1)) (*NIL*)))))) 
02600	EXPR)
02700	
02800	(DEFPROP >OPLIST< 
02900	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((>OPL< 1) (LIST (STK1) (QUOTE (:CH ;))))))))) 
03000	EXPR)
03100	
03200	(DEFPROP <OPL> 
03300	 (LAMBDA NIL
03400	  (NLRR (QUOTE OPL)
03500		(FUNCTION
03600		 (LAMBDA NIL
03700		  (COND ((AND (<OP>) (CH /,) (<OPL>)) (CONS (STK 2) (STK 0)))
03800			((AND (<OP>)) (CONS (STK 0) NIL))
03900			(*NIL*)))))) 
04000	EXPR)
04100	
04200	(DEFPROP >OPL< 
04300	 (LAMBDA(%N)
04400	  (OUTRUL %N
04500		  (FUNCTION
04600		   (LAMBDA NIL
04700		    (COND ((AND (MATCH (QUOTE (*))) (>OP< 0)) (STK0))
04800			  ((AND (MATCH (QUOTE (* . *))) (>OP< 1) (>OPL< 0)) (LIST (STK1) (QUOTE (:CH /,)) (STK0)))))))) 
04900	EXPR)
05000	
05100	(DEFPROP <OP> 
05200	 (LAMBDA NIL (NLRR (QUOTE OP) (ISITNM CONNECT))) 
05300	EXPR)
05400	
05500	(DEFPROP >OP< 
05600	 (LAMBDA (X) (OUTRUL X (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) CONNECT) NIL) (T (STK1))))))) 
05700	EXPR)
05800	
05900	(DEFPROP DECTBL 
06000	 (NIL (PRE_OP . PREFN) (EQUALITY .EQUAL)(PRE_PRED . PREPREDLET) (INF_OP . INFN) (INF_PRED . INFPREDLET) (VAR . IVAR)) 
06100	VALUE)
06200	
06300	(DEFPROP DECOP 
06400	 (NIL EQUALITY VAR INF_PRED INF_OP PRE_PRED PRE_OP) 
06500	VALUE)
06600	
06700	(DEFPROP <DECOP> 
06800	 (LAMBDA NIL (NLRR (QUOTE DECOP) (ISITM DECOP))) 
06900	EXPR)
07000	
07100	(DEFPROP >DECOP< 
07200	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) DECOP) (STK1))))))) 
07300	EXPR)
07400	
07500	(DEFPROP INCLAUSES 
07600	 (LAMBDA NIL
07700	  (PROG (Z Z1  AXNO)
07800		(SETQ AXNO (QUOTE AXIOM))
07900	   A    (SCANSET)
08000		(START)
08100		(SETQ ZIN (ERRSET (<INPUT>) T))
08200		(SCANRESET)
08300		(COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
08400		(SETQ ZIN (TOP))
08500		(COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z))
08600		      ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A))
08700		      ((MEMQ (CAR ZIN) DECOP) (GO B)))
08800		(OUT >S< ZIN)
08900		(SETQ Z
09000		      (APPEND Z
09100			      (SETUP
09200			       (CNF
09300				(COND ((EQ AXNO (QUOTE THEOREM)) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
09400		(GO A)
09500	   B    (SETQ Z1 (CDR (ASSOC (CAR ZIN) DECTBL)))
09600		(COND ((EQ Z1 (QUOTE IVAR)) (MAKOVAR (SETQ IVAR (CDR ZIN))))((EQ Z1 @EQUAL)(SETQ EQUAL(CADR ZIN))) (T (SET Z1 (CDR ZIN))))
09700		(OUT >INPUT< ZIN)
09800		(GO A))) 
09900	EXPR)